Lambda the Ultimate

Abstract Interface Types in GNAT: Conversions, Discriminants, and C++. Javier Miranda and Edmond Schonberg.

Ada 2005 Abstract Interface Types provide a limited and practical form of multiple inheritance of specifications. In this paper we cover the following aspects of their implementation in the GNAT compiler: interface type conversions, the layout of variable sized tagged objects with interface progenitors, and the use of the GNAT compiler for interfacing with C++ classes with compatible inheritance trees.

The addition of interface types, of the type found in Java, to Ada2005 presented compiler writers with an implementation challenge. This is a third paper in a series describing the implementation of interfaces in the GNAT Ada compiler (an earlier paper dealt with synchronized interfaces, an interesting special case).

The present paper deals mainly with issues caused by interface type conversions, and the related data layout issues. Of special interest is section 6 which shows how to write a C++/Ada multi-language program, in which method calls can be dispatched across language boundaries. Handling the multiple inheritance in the C++ code in this example is possible because the base classes have only pure virtual functions.

The theory LCF, for Logic of Computable Functions, was proposed by Dana Scott as a theory in the spirit of Church's simple theory of types which allows the computable functions to be characterised, and which comes with a rich enough logical theory to be analytically useful.

PCF, the Programming with Computable Functions toy language, was proposed by Robin Milner in an exposition of Scott's work on LCF.

The two formalisms have been enormously fruitful in theoretical computer science, and I've noticed that two of the early seminal papers are available as scanned PDFs:

• Robin Milner's 1973 Models of LCF; and
• Gordon Plotkin's 1977 LCF Considered as a Programming Language .

Dana Scott's original 1969 manuscript, A theory of computable functions of higher type was, I believe, only ever circulated informally, and I've never got hold of the manuscript in any form.

A Logic for Parametric Polymorphism, Gordon Plotkin and Martín Abadi.

In this paper we introduce a logic for parametric polymorphism. Just as LCF is a logic for the simply-typed lambda-calculus with recursion and arithmetic, our logic is a logic for System F. The logic permits the formal presentation and use of relational parametricity. Parametricity yields --- for example --- encodings of initial algebras, final co-algebras and abstract datatypes, with corresponding proof principles of induction, co-induction and simulation.

Another draft entry for HOPL-III about the The Development of the Emerald Programming Language by Andrew P. Black, Norman Hutchinson, Eric Jul and Henry M. Levy.

Emerald is an object-based programming language and system designed and implemented in the Department of Computer Science at the University of Washington in the early and mid-1980s. The goal of Emerald was to simplify the construction of distributed applications. This goal was re- flected at every level of the system: its object structure, the programming language design, the compiler implementation, and the run-time support.

This paper describes the origins of the Emerald group, the forces that formed the language, the influences that Emerald has had on subsequent distributed systems and programming languages, and some of Emerald’s more interesting technical innovations.

Worth a read for those interested in PL research topics which are still in play. Emerald explored a number of topics including distributed programming in the presence of failure; Mobile objects; Active objects; structural typing (as opposed to nominal); Static typing in the presence of open programming (shades of the ongoing work in Alice ML); Parametirized types. All of this while having performance as a top priority.

Previous links to HOPL-III papers.

The Structure and Value of Modularity in Software Design, K.J. Sullivan, W.G. Griswold, Y. Cai, B. Hallen.

The concept of information hiding modularity is a cornerstone of modern software design thought, but its formulation remains casual and its emphasis on changeability is imperfectly related to the goal of creating value in a given context. We need better models of the structure and value of information hiding, for both their explanatory power and prescriptive utility. We evaluate the potential of a new theory—developed to account for the influence of modularity on the evolution of the computer industry — to inform software design. The theory uses design structure matrices to model designs and real options techniques to value them. To test the potential utility of the theory for software we represent a model software system in its terms—Parnas’s KWIC—and evaluate the results. We contribute an extension to design structure matrices and show that the options results are consistent with Parnas’s conclusions. Our results suggest that such a theory does have potential to help inform software design.

This is really neat stuff; the authors use options theory to estimate the added value of a modular design relative to a less-modular design. It's always nice when an informal engineering intuition can be analyzed more precisely.

RZ: a tool for bringing constructive and computable mathematics closer to programming practice, Chris Stone and Andrej Bauer.

Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.

Realizability is a way of formalizing the constructive interpretation of logical formulas (eg, the BHK interpretation). Constructively, a proof of an implication A implies B means that if you are given evidence for A, you must be able to compute evidence for B. Since this constructive interpretation does not specify any particular programming language (theorists often use the lambda calculus, Turing machines, and the like) so Andrej Bauer and Chris Stone observed that they could take the realizers of mathematical proofs to be Objective Caml programs! This meant that they could take mathematical theories and generate ML module signatures describing the interface to the implementation of a mathematical theory, plus comments about what invariants must hold.

A paper by Charlotte Herzeel, Kris Gybels, Pascal Costanza presented at ILC2007.

Some program concerns cannot be cleanly modularized, and their implementation leads to code that is both hard to understand and maintain. In this paper we consider extending an e-commerce application, written in CLOS, with two of such crosscutting concerns. Though most of the time Common Lisp's macro facilities and CLOS method combinations can be used to modularize crosscuts, we discuss the use of a more declarative solution when crosscuts depend on the execution history. For this purpose we give an overview of HALO, a novel pointcut language based on logic meta programming and temporal logic, which allows one to reason about program execution and (past) program state.

Charlotte Herzeel presented this at ILC with a flashy web-shop application built on Edi Weitz's standard tools of the web trade. The example takes the basic web-shop and uses aspects to add a lot of funky rules about promotion and discounts based on stock levels, what's selling well, what the user has been browsing, etc, and makes sure the discounts are honoured at the checkout.

The focus on adding new and interesting functionality with aspects is refreshing. So is the basis in a powerful language like Lisp. The weakness of most aspect-oriented programming examples in my eyes is that they appear to be working around artificial problems caused by stubbornly using a base language that's ill-suited to the task. That only plays well with the audiences who are also stubbornly using those base languages for ill-suited tasks :-)

Cforall is a language design extending ISO C.

Cforall extends the C type-system using overloading, parametric polymorphism, and type generators. … [The] Cforall type system is based on parametric polymorphism, the ability to declare functions with type parameters, rather than an object-oriented type system.

Yesno: the other side ot the Gödelian coin

Any universally powerful programming language must either offer consistent semantics, or allow the possibility of programs not halting. … Almost all programming languages to date choose consistency. … Yesno is an inconsistent and complete programming language, and that every program returns a value.

NixOS is a Linux distribution based on Nix, a purely functional package management system. NixOS is an experiment to see if we can build an operating system in which software packages, configuration files, boot scripts and the like are all managaed in a purely functional way, that is, they are all built by deterministic functions and they never change after they have been built. Such an operating system should have all the nice characteristics that the Nix package manager has.

Here are links to:

• the Nix package manager webpage,
• the NixOS webpage, and
• Eelco Dolstra's PhD thesis, The Purely Functional Software Deployment Model.

I found this an extremely readable thesis, light on math but high on insight. I now have an entirely new way of thinking about components and the filesystem, and that's really cool. I'd be very interested in hearing what people with serious deployment/sysadmin experience think about this approach.

(Thanks to Gavin Mendel-Gleason and Martin Bravenboer for posting the original links in the discussions page!)